import Mathlib

variable (x : Nat)

-- 架构：陈伯昂
-- 感谢郝政伟与符逸铭两位大佬对架构提出的意见

lemma Nat.sq_of_isCoprime {x y z : ℕ} (h : x ^ 2 = y * z) (h_coprime : y.Coprime z) :
    ∃ a, y = a ^ 2 := by
  have h' : IsUnit (GCDMonoid.gcd y z) := by rwa [isUnit_iff_eq_one]
  obtain ⟨d, ⟨u, hu⟩⟩ := exists_associated_pow_of_mul_eq_pow h' h.symm
  use d
  simpa [Nat.units_eq_one u, Units.val_one, mul_one] using hu.symm

lemma Nat.exists_sq_of_coprime_mul_eq_sq {x y z : ℕ}
    (h : x ^ 2 = y * z) (h_coprime : y.Coprime z) (hy : y > 0) (hz : z > 0) :
    ∃ (a b : ℕ), a > 0 ∧ b > 0 ∧ a.Coprime b ∧ y = a ^ 2 ∧ z = b ^ 2 := by
  obtain ⟨a, ha⟩ := Nat.sq_of_isCoprime h h_coprime
  obtain ⟨b, hb⟩ := Nat.sq_of_isCoprime (by rw [mul_comm, h]) h_coprime.symm
  refine ⟨a, b, ?_, ?_, ?_, ha, hb⟩
  · rwa [gt_iff_lt, Nat.pos_iff_ne_zero, ← sq_pos_iff, ← ha]
  · rwa [gt_iff_lt, Nat.pos_iff_ne_zero, ← sq_pos_iff, ← hb]
  · rw [← Nat.isCoprime_iff_coprime, ← @IsCoprime.pow_iff _ _ _ _ 2 2 (by norm_num) (by norm_num)]
    rwa [ha, hb, ← Nat.isCoprime_iff_coprime] at h_coprime

lemma Nat.sq_pow_mod_four_eq_one_of_odd {x : ℕ} : Odd x → x ^ 2 % 4 = 1 := by
  intro hx
  obtain ⟨k, rfl⟩ := hx
  ring_nf
  simp

lemma Nat.sq_mod_four_eq_zero_of_even {x : ℕ} : Even x → x ^ 2 % 4 = 0 := by
  intro hx
  obtain ⟨k, rfl⟩ := hx
  ring_nf
  simp

lemma Nat.sq_mod_four_eq_one_or_zero (x : ℕ) : x ^ 2 % 4 = 1 ∨ x ^ 2 % 4 = 0 :=
  (Nat.even_or_odd x).elim (fun hx ↦ Or.inr (Nat.sq_mod_four_eq_zero_of_even hx))
    (fun hx ↦ Or.inl (sq_pow_mod_four_eq_one_of_odd hx))

theorem FermatLastTheoremTwo {x y z : ℕ} :
  x > 0 ∧ y > 0 ∧ z > 0 ∧ x.Coprime y ∧ 2 ∣ x ∧ x ^ 2 + y ^ 2 = z ^ 2 ↔ ∃ (a b : ℕ), a > 0 ∧ b > 0 ∧ a > b ∧ ((2 ∣ a ∧ ¬ 2 ∣ b) ∨ (¬ 2 ∣ a ∧ 2 ∣ b)) ∧ a.Coprime b ∧ x = 2 * a * b ∧ y = a ^ 2 - b ^ 2 ∧ z = a ^ 2 + b ^ 2 := by
    constructor
    · rintro ⟨xpos, ypos, zpos, xy_prime, x_two, xy_eq⟩
      have y_ntwo : y % 2 = 1 := by
        -- 黄文杰
        by_cases h_y_even : y % 2 = 0
        · have y_even : 2 ∣ y := Nat.dvd_of_mod_eq_zero h_y_even
          have two_dvd_gcd : 2 ∣ x.gcd y := Nat.dvd_gcd x_two y_even
          rw [xy_prime] at two_dvd_gcd
          norm_num at two_dvd_gcd
        · exact Nat.mod_two_ne_zero.mp h_y_even
      have z_ntwo : z % 2 = 1 := by
        -- 黄文杰
        have h_mod2 : (x ^ 2 + y ^ 2) % 2 = z ^ 2 % 2 := by rw [xy_eq]
        rw [Nat.add_mod] at h_mod2
        have x_pow_mod_zero : x ^ 2 % 2 = 0 := by
          rw [Nat.pow_mod, Nat.mod_eq_zero_of_dvd x_two]
        have y_pow_mod_one : y ^ 2 % 2 = 1 := by
          rw [Nat.pow_mod, y_ntwo]
        rw [x_pow_mod_zero, y_pow_mod_one] at h_mod2
        norm_num at h_mod2
        have h_z_sq_odd : z ^ 2 % 2 = 1 := h_mod2.symm
        by_cases h_z_even : z % 2 = 0
        · rw [Nat.pow_mod, h_z_even] at h_z_sq_odd
          norm_num at h_z_sq_odd
        · exact Nat.mod_two_ne_zero.mp h_z_even
      have yz_coprime : y.Coprime z := by
        -- 黄文杰
        apply Nat.coprime_of_dvd'
        intro p p_is_prime p_dvd_y p_dvd_z
        have p_dvd_x_sq : p ∣ x ^ 2 := by
          rw [← Nat.sub_eq_of_eq_add xy_eq.symm]
          have h_le : y ^ 2 ≤ z ^ 2 := by
            rw [← xy_eq, add_comm]
            exact Nat.le_add_right (y ^ 2) (x ^ 2)
          have p_dvd_y_sq : p ∣ y ^ 2 := dvd_pow p_dvd_y (by norm_num)
          have p_dvd_z_sq : p ∣ z ^ 2 := dvd_pow p_dvd_z (by norm_num)
          exact (Nat.dvd_sub_iff_left h_le p_dvd_y_sq).mpr p_dvd_z_sq
        have p_dvd_x : p ∣ x :=
          p_is_prime.dvd_of_dvd_pow p_dvd_x_sq
        have p_dvd_gcd_xy : p ∣ x.gcd y :=
          Nat.dvd_gcd p_dvd_x p_dvd_y
        rw [xy_prime.gcd_eq_one] at p_dvd_gcd_xy
        exact p_dvd_gcd_xy
      let m := (z + y) / 2
      let n := (z - y) / 2
      have mn_coprime : m.Coprime n := by
        -- 张湧鹏已认领
        sorry
      have eq : (x / 2) ^ 2 = m * n := by
        -- 张湧鹏已认领
        sorry
      have x_pow_pos : (x / 2) ^ 2 > 0 := by
        apply Nat.pow_pos
        field_simp
        -- 郝政伟
        omega
      have mpos : m > 0 := by
        unfold m
        field_simp
        linarith
      have npos : n > 0 := by
        unfold n
        field_simp
        -- 郝政伟
        have h_z_gt_y : y < z := by
          have h_sq_lt : y ^ 2 < z ^ 2 := by
              calc
                y ^ 2 < y ^ 2 + x ^ 2       := by apply lt_add_of_pos_right;exact Nat.pow_pos xpos
                _       = z ^ 2             := by rw [add_comm, xy_eq]
          exact lt_of_pow_lt_pow_left' 2 h_sq_lt
        omega
      have mn_pow2 : ∃ (a b : ℕ), a > 0 ∧ b > 0 ∧ a.Coprime b ∧ m = a ^ 2 ∧ n = b ^ 2 := by
        exact Nat.exists_sq_of_coprime_mul_eq_sq eq mn_coprime mpos npos
      rcases mn_pow2 with ⟨a, b, apos, bpos,ab_prime, m_pow2, n_pow2⟩
      have aleb : a > b := by
        -- 张湧鹏已认领

        sorry
      have a_add_b_ntwo : (a + b) % 2 = 1 := by
        -- 郝政伟已认领
        have h_sum : a ^ 2 + b ^ 2 = z := by
          rw [← m_pow2, ← n_pow2]
          unfold m n
          have h_z_gt_y : y < z := by
            have h_sq_lt : y ^ 2 < z ^ 2 := by
                calc
                  y ^ 2 < y ^ 2 + x ^ 2       := by apply lt_add_of_pos_right;exact Nat.pow_pos xpos
                  _       = z ^ 2             := by rw [add_comm, xy_eq]
            exact lt_of_pow_lt_pow_left' 2 h_sq_lt
          have h_le : y ≤ z := by exact Nat.le_of_succ_le h_z_gt_y
          apply Nat.mul_left_cancel (show 2 > 0 by decide)
          rw [Nat.mul_add]
          have h_dvd_add : 2 ∣ z + y := by
            rw [Nat.dvd_iff_mod_eq_zero, Nat.add_mod, z_ntwo, y_ntwo]
          have h_dvd_sub : 2 ∣ z - y := by
            rw [Nat.dvd_iff_mod_eq_zero]
            have h1 : z % 2 = 1 := z_ntwo
            have h2 : y % 2 = 1 := y_ntwo
            have h8 : (z - y) % 2 = 0 := by
              omega
            exact h8
          rw [Nat.mul_div_cancel' h_dvd_add, Nat.mul_div_cancel' h_dvd_sub]
          omega
        calc (a + b) % 2
          _ = (a % 2 + b % 2) % 2           := by rw [Nat.add_mod]
          _ = (a ^ 2 % 2 + b ^ 2 % 2) % 2   := by
              have h1 : a % 2 = 0 ∨ a % 2 = 1 := by omega
              have h2 : b % 2 = 0 ∨ b % 2 = 1 := by omega
              rcases h1 with (h1 | h1) <;> rcases h2 with (h2 | h2) <;> simp [Nat.pow_mod, Nat.add_mod, h1, h2, Nat.mul_mod]
          _ = (a ^ 2 + b ^ 2) % 2           := by rw [← Nat.add_mod]
          _ = z % 2                         := by rw [h_sum]
          _ = 1                             := z_ntwo
      have ab_ntwo : (2 ∣ a ∧ ¬2 ∣ b ∨ ¬2 ∣ a ∧ 2 ∣ b) := by
        have h1 : (a : ℕ) % 2 = 0 ∨ (a : ℕ) % 2 = 1 := by omega
        have h2 : (b : ℕ) % 2 = 0 ∨ (b : ℕ) % 2 = 1 := by omega
        omega
      use a
      use b
      have xeq : x = 2 * a * b := by
        -- 郝政伟已认领
        rw [m_pow2, n_pow2, ←mul_pow] at eq
        have h_div_eq : x / 2 = a * b := (Nat.pow_left_inj (by norm_num)).mp eq
        rw [mul_assoc]
        rw [←h_div_eq]
        exact (Nat.mul_div_cancel' x_two).symm
      have yeq : y = a ^ 2 - b ^ 2 := by
        -- 彭炜
        sorry
      have zeq : z = a ^ 2 + b ^ 2 := by
        -- 彭炜
        sorry
      exact ⟨apos, bpos, aleb, ab_ntwo, ab_prime, xeq, yeq, zeq⟩
    · intro h
      rcases h with ⟨a, b, apos, bpos, aleb, hab⟩
      rcases hab with ⟨ab_two, ab_prime, xeq, yeq, zeq⟩
      constructor
      · show x > 0
        -- 彭炜
        sorry
      constructor
      · show y > 0
        -- 彭炜
        sorry
      constructor
      · show z > 0
        -- 彭炜
        sorry
      constructor
      · show x.Coprime y
        -- 张湧鹏
        sorry
      constructor
      · use (a * b)
        rw [← mul_assoc]
        exact xeq
      · rw [xeq, yeq, zeq]
        repeat rw [pow_two]
        -- 张湧鹏
        sorry

lemma FermatLastTheoremFour_case :
  ∀ x y u : ℕ, x > 0 → y > 0 → u > 0 → x.Coprime y → x ^ 4 + y ^ 4 ≠ u ^ 2 := by
    suffices ∀ u, ∀ x y, x > 0 → y > 0 → u > 0 → x.Coprime y → x ^ 4 + y ^ 4 ≠ u ^ 2 by
      intro x y u hx hy hu h_coprime
      exact this u x y hx hy hu h_coprime
    intro u_val
    induction' u_val using Nat.strong_induction_on with u' ih
    intro x y
    intro xpos ypos
    intro u'_pos
    intro xy_prime
    intro contra
    have u_two : u' % 2 = 1 := by
      have contra_mod_4 := congr_arg (fun n => n % 4) contra
      revert contra_mod_4
      rcases (Nat.even_or_odd x) with (hx | hx)
      · rcases (Nat.even_or_odd y) with (hy | hy)
        · have : 2 ∣ x.gcd y :=by
            -- 彭炜
            sorry
          rw [xy_prime.gcd_eq_one] at this
          norm_num at this
        · have h1: x ^ 4 % 4 = 0 := by
            -- 张湧鹏
            sorry
          have h2: y ^ 4 % 4 = 1 := by
          -- 王寅沣
            rcases Nat.even_or_odd y with ⟨k, rfl⟩ | ⟨k, rfl⟩
            . have pow4_even : (k+k)^4 = 4 * (4 * k^4) := by ring
              rw [pow4_even]
              sorry
            . have pow4_odd : (2*k + 1)^4 = 1 + 4 * (4*k^3 + 6*k^2 + 2*k) := by sorry
              rw [pow4_odd, Nat.add_mul_mod_self_left]
          intro h
          have h3: (x ^ 4 + y ^ 4) % 4 = 1 := by rw [Nat.add_mod, h1, h2]
          simp [h3] at h
          have h1 : u' ^ 2 % 4 = 1 := by
            omega
          by_contra h2
          push_neg at h2
          have h2' : u' % 2 = 0 := by
            omega
          have h3 : u' ^ 2 % 4 = 0 := by
            have h4 : u' % 2 = 0 := h2'
            have h5 : ∃ k, u' = 2 * k := by
              refine ⟨u' / 2, by omega⟩
            rcases h5 with ⟨k, hk⟩
            rw [hk]
            ring_nf
            omega
          omega
      · rcases (Nat.even_or_odd y) with (hy | hy)
        · -- 王寅沣
          sorry
        · -- 王寅沣
          sorry
    have xy_two : (2 ∣ x ∧ ¬ 2 ∣ y) ∨ (¬ 2 ∣ x ∧ 2 ∣ y) := by
      -- 符逸铭
      suffices ¬ ((2 ∣ x ∧ 2 ∣ y) ∨ (¬ 2 ∣ x ∧ ¬ 2 ∣ y)) by tauto
      intro h
      rcases h with ⟨hx, hy⟩ | ⟨hx, hy⟩
      · absurd xy_prime
        exact Nat.Prime.not_coprime_iff_dvd.mpr ⟨2, by norm_num, ⟨hx, hy⟩⟩
      · rw [Nat.two_dvd_ne_zero] at hx hy
        replace hx : x ^ 4 % 4 = 1 := by
          rw [pow_mul x 2 2]
          apply Nat.sq_pow_mod_four_eq_one_of_odd
          exact Odd.pow <| Nat.odd_iff.mpr hx
        replace hy : y ^ 4 % 4 = 1 := by
          rw [pow_mul y 2 2]
          apply Nat.sq_pow_mod_four_eq_one_of_odd
          exact Odd.pow <| Nat.odd_iff.mpr hy
        replace contra : u' ^ 2 % 4 = 2 := by
          rw [← contra, Nat.add_mod_of_add_mod_lt, hx, hy]
          rw [hx, hy] ; norm_num
        absurd contra
        exact (Nat.sq_mod_four_eq_one_or_zero u').elim (fun h ↦ by rw [h] ; norm_num)
          (fun h ↦ by rw [h] ; norm_num)
    have xy_pow_prime : (x ^ 2).Coprime (y ^ 2) := by
      -- 陈伯昂
      exact Nat.pow_gcd_pow_of_gcd_eq_one xy_prime
    wlog h_parity : 2 ∣ x ∧ ¬ 2 ∣ y generalizing x y with H
    · rcases xy_two with (h1 | h2)
      · contradiction
      · apply H y x
        exact id (And.symm h2)
        exact ypos
        exact xpos
        exact Nat.coprime_comm.mp xy_prime
        rw [add_comm] at contra
        exact contra
        exact Or.symm (Or.inr (id (And.symm h2)))
        exact Nat.coprime_comm.mp xy_pow_prime
    · have x_pow_pos : x ^ 2 > 0 := sq_pos_of_pos xpos -- 郭际泽
      have y_pow_pos : y ^ 2 > 0 := sq_pos_of_pos ypos -- 郭际泽
      have x_pow_two : 2 ∣ x ^ 2 := dvd_pow h_parity.left (by decide) -- 郭际泽
      have eq_pow2 : (x ^ 2) ^ 2 + (y ^ 2) ^ 2 = u' ^ 2 := by
        -- 郭际泽
        rw [← pow_mul, ← pow_mul, contra]
      have pyth_triple_x2y2 :
        ∃ a b : ℕ, a > 0 ∧ b > 0 ∧ a > b
        ∧ ((2 ∣ a ∧ ¬ 2 ∣ b) ∨ (¬ 2 ∣ a ∧ 2 ∣ b))
        ∧ a.Coprime b
        ∧ x ^ 2 = 2 * a * b
        ∧ y ^ 2 = a ^ 2 - b ^ 2
        ∧ u' = a ^ 2 + b ^ 2 := by
        -- 郭际泽
        apply FermatLastTheoremTwo.mp
        tauto
      rcases pyth_triple_x2y2 with ⟨a, b, apos, bpos, aleb, hab⟩
      rcases hab with ⟨ab_parity, ab_prime, xeq, yeq, ueq⟩
      rcases ab_parity with (ab_even_odd | ab_odd_even)
      · have y_mod_four_one : y ^ 2 % 4 = 1 := by
          -- 周浩然
          sorry
        have y_mod_four_not_one : y ^ 2 % 4 ≠ 1 := by
          -- 周浩然
          sorry
        contradiction
      · rcases ab_odd_even with ⟨a_ntwo, ⟨c, ceq⟩⟩
        have c_pos : c > 0 := by
          -- 周浩然
          sorry
        have eq_ac : (x / 2) ^ 2 = a * c := by
          -- 周浩然
          sorry
        have ac_prime : a.Coprime c := by
          -- 周浩然
          apply Nat.coprime_of_dvd'
          intro p p_is_prime p_dvd_a p_dvd_c
          have p_dvd_b : p ∣ b := by
            rw [ceq]
            exact dvd_mul_of_dvd_right p_dvd_c 2
          have p_dvd_gcd_ab : p ∣ a.gcd b := Nat.dvd_gcd p_dvd_a p_dvd_b
          rw [ab_prime.gcd_eq_one] at p_dvd_gcd_ab
          exact p_dvd_gcd_ab
        have ac_are_squares : ∃ d f : ℕ, d > 0 ∧ f > 0 ∧ d.Coprime f ∧ a = d ^ 2 ∧ c = f ^ 2 := by
          exact Nat.exists_sq_of_coprime_mul_eq_sq eq_ac ac_prime apos c_pos
        rcases ac_are_squares with ⟨d, f, dpos, fpos, df_coprime, d_pow2, f_pow2⟩
        have f_pow_pos : 2 * f ^ 2 > 0 := by
          -- 黄文杰
          apply mul_pos
          · norm_num
          · exact pow_pos fpos 2
        have d_pow_pos : d ^ 2 > 0 := by
          -- 黄文杰
          apply pow_pos
          exact dpos
        have dfy_coprime : (2 * f ^ 2).Coprime y := by
          -- 缪诗妍
          sorry
        have f_pow_two : 2 ∣ 2 * f ^ 2 := by
          -- 缪诗妍
          sorry
        have eq_dfy : (2 * f ^ 2) ^ 2 + y ^ 2 = (d ^ 2) ^ 2 := by
          -- 缪诗妍
          calc
          (2 * f ^ 2)^2 + y ^ 2
          _ = (2 * c) ^ 2 + y ^ 2 := by rw [←f_pow2] -- 使用 f_pow2 将 f^2 替换为 c
          _ = b ^ 2 + y ^ 2 := by rw [←ceq] -- 使用 ceq 将 2 * c 替换为 b
          _ = a ^ 2 := by rw [yeq];omega
          _ = (d ^ 2) ^ 2 := by rw [d_pow2]
        have pyth_triple_2f2y : ∃ l m : ℕ, l > 0 ∧ m > 0 ∧ l > m ∧ ((2 ∣ l ∧ ¬ 2 ∣ m) ∨ (¬ 2 ∣ l ∧ 2 ∣ m)) ∧ l.Coprime m ∧ 2 * f ^ 2 = 2 * l * m ∧ y = l ^ 2 - m ^ 2 ∧ d ^ 2 = l ^ 2 + m ^ 2 := by
          -- 缪诗妍
          sorry
        rcases pyth_triple_2f2y with ⟨l, m, lpos, mpos, llem, hlm⟩
        rcases hlm with ⟨lm_parity, lm_prime, feq, yeq2, deq⟩
        have eq_lm : f ^ 2 = l * m := by
          -- 缪诗妍
          sorry
        have lm_are_squares : ∃ r s : ℕ, l = r ^ 2 ∧ m = s ^ 2 := by
          -- 王寅沣
          sorry
        rcases lm_are_squares with ⟨r, s, r_pow2, s_pow2⟩
        have rpos : r > 0 := by
          -- 王寅沣
          sorry
        have spos : s > 0 := by
          -- 王寅沣
          sorry
        have rs_prime : r.Coprime s := by
          --郭际泽
          -- we have gcd(l, m) = 1
          -- we have l = r ^ 2, m = s ^ 2, so gcd(l, m) = gcd(r, s) ^ 2
          -- then gcd(r, s) = 1
          have : (r.gcd s) * (r.gcd s) = 1 := by
            rw [← pow_two, ← Nat.pow_gcd_pow, ← r_pow2, ← s_pow2, lm_prime]
          refine Nat.eq_one_of_mul_eq_one_left this
        have little_eq : r ^ 4 + s ^ 4 = d ^ 2 := by
          --郭际泽
          -- we have d ^ 2 = l ^ 2 + m ^ 2, l = r ^ 2, m = s ^ 2
          -- the conclusion follows from simple algebra
          rw [deq, r_pow2, s_pow2, ← Nat.pow_mul, ← Nat.pow_mul]
        have d_lt_u' : d < u' := by
          --郭际泽
          -- straightforward inequality chain
          calc d
            _ ≤ d ^ 2 := Nat.le_pow (show 0 < 2 by decide)
            _ = a := by rw [d_pow2]
            _ ≤ a ^ 2 := Nat.le_pow (show 0 < 2 by decide)
            _ < a ^ 2 + b ^ 2 := Nat.lt_add_of_pos_right (Nat.pow_pos bpos)
            _ = u' := by rw [ueq]
        specialize ih d d_lt_u'
        have final_contradiction := ih r s rpos spos dpos rs_prime
        exact final_contradiction little_eq

-- 郝政伟
theorem FermatLastTheoremFour :
  ∀ x y z : ℕ, x > 0 → y > 0 → z > 0 → x ^ 4 + y ^ 4 ≠ z ^ 4 := by
    intro x y z hx hy hz h_contra
    let g := x.gcd y
    have hg_pos : g > 0 := Nat.gcd_pos_of_pos_left y hx
    let x' := x / g
    let y' := y / g
    have h_coprime : x'.Coprime y' := Nat.gcd_div_gcd_div_gcd_of_pos_right hy
    have hg_dvd_z : g ∣ z := by
      have hg4_dvd_z4 : g ^ 4 ∣ z ^ 4 := by
        use (x' ^ 4 + y' ^ 4)
        have hx_eq : x = g * x' := (Nat.mul_div_cancel' (Nat.gcd_dvd_left x y)).symm
        have hy_eq : y = g * y' := (Nat.mul_div_cancel' (Nat.gcd_dvd_right x y)).symm
        rw [h_contra.symm, hx_eq, hy_eq, mul_pow, mul_pow, ← mul_add]
      exact (Nat.pow_dvd_pow_iff (by omega)).mp hg4_dvd_z4
    let z' := z / g
    have h_primitive_eq : x' ^ 4 + y' ^ 4 = z' ^ 4 := by
      have hx_eq := (Nat.mul_div_cancel' (Nat.gcd_dvd_left x y)).symm
      have hy_eq := (Nat.mul_div_cancel' (Nat.gcd_dvd_right x y)).symm
      have hz_eq := (Nat.mul_div_cancel' hg_dvd_z).symm
      have hh := pow_pos hg_pos 4
      have hh2 :  g ^ 4 ≠ 0 := Nat.ne_zero_of_lt hh
      apply (Nat.mul_right_inj (Nat.ne_zero_of_lt (pow_pos hg_pos 4))).mp
      rw [mul_add, ← mul_pow, ← mul_pow, ← hx_eq, ← hy_eq, h_contra, hz_eq, mul_pow]
    have hx'_pos : x' > 0 := Nat.div_gcd_pos_of_pos_left y hx
    have hy'_pos : y' > 0 := Nat.div_gcd_pos_of_pos_right x hy
    have hz'_pos : z' > 0 := (Nat.lt_div_iff_mul_lt' hg_dvd_z 0).mpr hz
    let u := z' ^ 2
    have hu_pos : u > 0 := pow_pos hz'_pos 2
    have h_final_eq : x' ^ 4 + y' ^ 4 = u ^ 2 := by
      rw [h_primitive_eq]
      unfold u
      rw [← pow_mul]
    exact FermatLastTheoremFour_case x' y' u hx'_pos hy'_pos hu_pos h_coprime h_final_eq
